{- «•»«•»«•»«•»«•»«•»«•»«•»«•»«•»«•»«•»«•»«•»«•»«•»«•»«•»«•»«•»«•»«•»«•»«•»

    Copyright © 2011 - 2021, Ingo Wechsung
    All rights reserved.

    Redistribution and use in source and binary forms, with or
    without modification, are permitted provided that the following
    conditions are met:

        Redistributions of source code must retain the above copyright
        notice, this list of conditions and the following disclaimer.

        Redistributions in binary form must reproduce the above
        copyright notice, this list of conditions and the following
        disclaimer in the documentation and/or other materials provided
        with the distribution. Neither the name of the copyright holder
        nor the names of its contributors may be used to endorse or
        promote products derived from this software without specific
        prior written permission.

    THIS SOFTWARE IS PROVIDED BY THE
    COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR
    IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
    WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
    PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER
    OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
    SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
    LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF
    USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED
    AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
    LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING
    IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF
    THE POSSIBILITY OF SUCH DAMAGE.

    «•»«•»«•»«•»«•»«•»«•»«•»«•»«•»«•»«•»«•»«•»«•»«•»«•»«•»«•»«•»«•»«•»«•»«•» -}

{--
 * Properties of the _Prelude_.
 -}


package tests.qc.PreludeProperties where

import Data.List 

import frege.prelude.Math (floor)
-- import Test.QuickCheckArbitrary ()
import Test.QuickCheck 

trivial = (`classify` "trivial")

--* a generator for all 16-bit characters
chars = arbitrary::Gen Char
strings = arbitrary::Gen String
ints = arbitrary::Gen Int
longs = arbitrary::Gen Long
integers = arbitrary::Gen Integer
floats = arbitrary::Gen Float
doubles = arbitrary::Gen Double
lists = arbitrary :: Gen [Int]
ssLists = arbitrary :: Gen [(Small, Small)]
sLists = arbitrary :: Gen [Small]
funs = elements (zipWith Fun [(Int.+), (Int.subtract), Int.min, Int.max] ["+", "subtract", "min", "max"])
tupleLists = arbitrary :: Gen [(Int, String)]

data Fun a = Fun a String
instance Show (Fun a) where
    show (Fun f s) = "function " ++ s 

data Small = SA | SB | SC | SD | SE | SF | SG | SH | SI | SJ | SK | SL | SM
derive Show Small
derive Enum Small
instance Arbitrary Small where
    arbitrary = elements [SA .. SM]

instance CoArbitrary Small where
    coarbitrary n = variant (ord n)

-- funs  = oneof [(Int.+), (-)::Int->Int->Int, Int.min, Int.max] :: Gen (Int->Int->Int)

--- @(c::Char).ord.char == c@
p_OrdChar = forAll chars (\c -> c.ord.char == c)
--* round d == (long) floor (d + 0.5)
p_DoubleRoundFloor = forAll doubles (\d ->
        (d < Long.maxBound.double && d > Long.minBound.double) ==>
            (d.long.double == (d+0.5).floor))
p_FloatRoundFloor = forAll floats (\f ->
        (f < Int.maxBound.float && f > Int.minBound.float) ==>
        (f.int.float == (f+0.5f).floor.float))
--- if m.group n is Nothing, then m.start m < 0
p_MatcherGroupStartEnd1 = forAll strings (\s ->
         case s =~ ´(x)|(.)´ of
            Nothing -> trivial true true
            Just m  -> m.group 1 == Nothing ==> m.start 1 < 0 && m.start 1 == m.end 1
         )
--- the matched string is the same as the
--- substring obtained with 'Matcher.start' and 'Matcher.end'
p_MatcherGroupStartEnd2 = forAll strings (\s ->
        case s =~ ´([a-zA-Z]+)|(.)´ of
            Nothing -> trivial true true
            Just m
                | Just r <- m.group 1 = label "matches" (r == substr s (m.start 1) (m.end 1))
                | otherwise = property true
         )

--- after a successful match @m.match == unJust (m.group 0)@
p_MatcherEquivMatchGroup0 = property (\s ->
        case s =~ ´\w+´ of
            Nothing -> trivial true true
            Just m -> label "matches" (m.match == unJust (m.group 0))
    )

--- the remainder has the same sign as the divident and @(a quot b)*b+(a rem b) == a@
integralRemainder gen = forAll gen (\a -> forAll gen (\b ->
    if b == zero then label "zero divisor" true
    else if a `rem` b == zero then label "zero remainder" true
    else let r = a `rem` b in
        property $! (a `quot` b) * b + r == a && (a <=> zero) == (r <=> zero)
    ))

--- @(a div b)*b+(a mod b) == a@
integralDivMod gen = forAll gen (\a -> forAll gen (\b ->
    if b == zero then label "zero divisor" true
    else if a `mod` b == zero then label "zero modulus" true
    else let r = a `mod` b in
        property $! (a `div` b) * b + r == a
    ))

--- @(a rem b)@ and @(a mod b)@ differ by at most 1
integralQuoteDiv gen = forAll gen (\a -> forAll gen (\b ->
    if b == zero then label "zero divisor" true
    else let q = a `quot` b
             d = a `div` b
        in
        property $! q == d || q-one == d
    ))

p_IntRemainder     = integralRemainder ints
p_LongRemainder    = integralRemainder longs
p_IntegerRemainder = integralRemainder integers
p_IntDivMod        = integralDivMod ints
p_LongDivMod       = integralDivMod longs
p_IntegerDivMod    = integralDivMod integers
p_IntQuoteDiv        = integralQuoteDiv ints
p_LongQuoteDiv       = integralQuoteDiv longs
p_IntegerQuoteDiv    = integralQuoteDiv integers


--- 'mod' works the same way on Int and Integer
p_ModImplementation = forAll ints (\a -> forAll ints (\b ->
        b != 0 ==> (a `mod` b).big == (a.big `mod` b.big)
    ))

derive Show (a, b, c, d)
derive Eq   (a, b, c, d)
--- Eq -- this should hold for all types
p_Equality = forAll (arbitrary::Gen (Int, Double, [Char], String))
     (\a -> forAll arbitrary (\b ->
        (a == a)
        && !(a != a)
        && (a != b) == !(a == b)
        && (a == b) != (a != b)
        ))

--- this property should hold for all instances of Ord
p_Ord1 = forAll ints (\a -> forAll ints (\b ->
        case a <=> b of
            Eq -> label "equal"     (a == b)
            _  -> label "not equal" (a != b)
    ))

p_OrdLt1 = forAll floats (\a -> forAll arbitrary (\b  -> forAll arbitrary (\c  ->
        let
            -- b = a + a
            -- c = (b + a) `div` 2
            assumption = (a < b && b < c)
        in if assumption then  property (a < c) -- (assumption ==> (a < c))
            else label "trivial" true
    )))
p_OrdLtGt = forAll strings (\a -> forAll arbitrary (\b -> (a < b) == (b > a)))
p_OrdLe1 = forAll doubles (\a -> forAll arbitrary (\b  -> forAll arbitrary (\c  ->
        let
            assumption = (a <= b && b <= c)
        in if assumption then  property (a <= c)
            else label "trivial" true
    )))
p_OrdLe2 = forAll longs (\a -> forAll arbitrary (\b -> (a <= b) == (b >= a)))
p_OrdLe3 = forAll integers (\a -> forAll arbitrary (\b -> (a <= b) == !(a > b)))
p_OrdGt1 = forAll chars (\a -> forAll arbitrary (\b  -> forAll arbitrary (\c  ->
        let
            assumption = (a > b && b > c)
        in if assumption then  property (a > c) -- (assumption ==> (a < c))
            else label "trivial" true
    )))
p_OrdGe1 = forAll (arbitrary::Gen (Maybe String)) (\a -> forAll arbitrary (\b  -> forAll arbitrary (\c  ->
        let
            assumption = (a >= b && b >= c)
        in if assumption then  property (a >= c)
            else label "trivial" true
    )))
p_OrdGe2 = forAll (arbitrary::Gen (Either [Char] (Maybe String)))
    (\a -> forAll arbitrary
        (\b -> (a >= b) == (b <= a)))
p_OrdGe3 = forAll (arbitrary::Gen [String]) (\a -> forAll arbitrary (\b -> (a >= b) == !(a < b)))
p_Ordmin = forAll ints (\a -> forAll arbitrary (\b ->
            min a b == (if a < b then a else b)
        ))
p_Ordmax = forAll ints (\a -> forAll arbitrary (\b ->
            max a b == (if a > b then a else b)
        ))

p_Negate arb = forAll arb (\a -> isNumber a ==> (a + negate a == zero))
p_NegInt    = p_Negate ints
p_NegLong   = p_Negate longs
p_NegFloat  = p_Negate floats
p_NegDouble = p_Negate doubles
p_NegBig    = p_Negate integers

p_initLast = forAll lists (\xs ->
    if null xs
        then label "not applicable" true
        else label "not empty" (init xs ++ [last xs] == xs))
p_scanlFold = forAll funs (\(Fun f _) ->
    forAll lists (\xs ->
        property (\z ->
            trivial (null xs) $ last (scanl f z xs) == fold f z xs)))

p_foldrFoldrs = forAll funs (\(Fun f _) ->
    forAll lists (\xs ->
        property (\z -> trivial (null xs) $ foldr f z xs == foldrs f z xs)))

p_revRev = forAll lists (\xs -> trivial (null xs) $ xs == reverse (reverse xs))

p_Any = forAll lists (\xs -> trivial (null xs) $ any f xs == fold (||) false (map f xs))
    where f i = i `mod` 2 == 0

p_All = forAll lists (\xs -> trivial (null xs) $
        classify (all f xs) "true cases" $
        classify (any (not•f) xs) "false cases" $ all f xs == fold (&&) true (map f xs))
    where f i = i `mod` 5 != 0

p_takeDrop = forAll lists (\xs -> property (\n ->
        classify (null xs) "empty list" $
        classify (n < 0) "not applicable due to negative n" $
        classify (n == 0) "zero n" $
        classify (n >= length xs) "whole list" $
        (n >= 0 ==> take n xs ++ drop n xs == xs)))

p_takeDropW = forAll lists (\xs ->
        classify (null xs) "empty list" $
        classify (not (null xs) && f (head xs)) "at least 1 taken/dropped" $
        (takeWhile f xs ++ dropWhile f xs == xs))
    where  f i = i `mod` 2 == 0

p_takeDropU = forAll lists (\xs ->
        classify (null xs) "empty list" $
        classify (not (null xs) && f (head xs)) "nothing taken/dropped" $
        (takeUntil f xs ++ dropUntil f xs == xs))
    where  f i = i `mod` 5 == 0

p_Span = forAll lists (\xs ->
        classify (null xs) "empty list" $
        classify (((0==) • length • takeWhile f) xs)  "none taken" $
        classify (((1==) • length • takeWhile f) xs)  "one taken" $
        classify (((1<) • length • takeWhile f) xs)  "some taken" $
        (span f xs == (takeWhile f xs, dropWhile f xs)))
    where  f i = i `mod` 5 != 0

p_Chunk = forAll lists (\xs -> 
        property (\n -> 
            n != 0 ==> concat (chunked (abs n) xs) == xs))

p_Elem = forAll lists (\es -> property (\e ->
        e `elem` es == any (e==) es))

p_notElem = forAll lists (\es -> property (\e ->
        e `notElem` es == all (e!=) es))

p_Unique = forAll sLists (\es -> trivial (null es) $
    classify (all ((<2) • length) (group es)) "no duplicates" $
    sort (unique es) == uniq (sort es))

p_UniqueBy = forAll ssLists (\es -> trivial (null es) $
    classify (all ((<2) • length) (groupBy (using fst) es)) "no duplicates" $
    sortBy (comparing fst) (uniqueBy (using fst) es) == uniqBy (using fst) (sortBy (comparing fst) es))

p_Sort = forAll ssLists (\xs -> case uniqueBy (using fst) xs of {
    ss -> sortBy (ascending fst) ss == reverse (sortBy (descending fst) ss)}) 

p_Partition = forAll lists (\xs -> let ps = partitioned p xs in
        classify (null (fst ps)) "empty left partition" $
        classify (null (snd ps)) "empty right partition" $
         all p (fst ps)
        && (not • any p) (snd ps)
        && length (fst ps) + length (snd ps) == length xs
        && all (`elem` xs) (fst ps)
        && all (`elem` xs) (snd ps)
        && all (\x -> x `elem` fst ps || x `elem` snd ps) xs)
    where p i = i `mod` 3 == 0

p_Packed = forAll strings (\s ->
        trivial (null s) $
        packed (unpacked s) == s)

p_Zip = forAll tupleLists (\xs ->
        (uncurry zip • unzip) xs == xs)

--- some examples taken from Data.List
p_DataList = property (and [uniqueBy (==) "abrakadabra".toList == "abrkd".toList,
                "dog".toList `union` "cow".toList == unpacked "dogcw",
                [1,2,3,4]   `intersect` [2,4,6,8] == [2,4],
                [1,2,2,3,4] `intersect` [6,4,4,2] == [2,2,4],
                isInfixOf "Haskell".toList "I really like Haskell.".toList == true,
                isInfixOf "lkFrg".toList   "I like Frege still more.".toList == false,
                ])
p_listDiff = property difflaw where
    difflaw :: [Char] -> [Char] -> Bool
    difflaw xs ys = 
        (xs ++ ys) \\ xs == ys

--- 'comparing' _f_ is the same as ('<=>') `'on'` _f_
p_comparingOn = property p where
    p :: Int -> Int -> Bool
    p a b = comparing negate a b == ((<=>) `on` negate) a b
    
p_True = once true

--- 'words' does not deliver empty elements
p_words = property w where
    w s = trivial (s ~ '^\S') $ all (not . null) (words s)
    
         
main _ = do
        -- stop at first failed test
        allSingle  <- foldM (checkAnd 1) true singleChecks
        allLaws   <- foldM (checkAnd 500) true laws
        allChecks <- foldM (checkAnd 500) allLaws checks
        shrtChcks <- foldM (checkAnd 100) allChecks shortChecks
        if (allSingle && allLaws && allChecks && shrtChcks) 
          then println "All tests passed."
          else System.exit 1
    where
        checkAnd n false prop = return false
        checkAnd n true  prop = quickCheckWithResult stdArgs.{maxSuccess = n} prop
                                    >>= return . isSuccess
        singleChecks = [p_DataList]
        laws = [ p_MatcherEquivMatchGroup0, p_listDiff ]
        checks = [ p_OrdChar, p_DoubleRoundFloor, p_Equality, p_FloatRoundFloor,
            p_IntRemainder, p_IntegerRemainder, p_LongRemainder,
            p_IntDivMod, p_IntegerDivMod, p_LongDivMod,
            p_IntQuoteDiv, p_IntegerQuoteDiv, p_LongQuoteDiv,
            p_MatcherGroupStartEnd1,
            p_MatcherGroupStartEnd2,
            p_ModImplementation,    p_NegBig,    p_NegDouble,    p_NegFloat,
            p_NegInt,    p_NegLong,    p_Ord1,    p_OrdChar,    p_OrdGe1,
            p_OrdGe2,    p_OrdGe3,    p_OrdGt1,    p_OrdLe1,    p_OrdLe2,    p_OrdLe3,
            p_OrdLt1,    p_OrdLtGt,    p_Ordmax,    p_Ordmin,
            p_initLast,  p_scanlFold,  p_foldrFoldrs, p_revRev, p_Any, p_All,
            p_takeDrop, p_takeDropW, p_takeDropU, p_Span, p_Chunk,
            p_Elem, p_notElem, p_Unique, p_UniqueBy,
            p_Sort,
            p_Partition, p_Packed]
        shortChecks = [p_Zip]
